1. $A$ : Type
\\[0ex]2. $B$ : Type
\\[0ex]3. $f$ : $A$$\rightarrow$$B$
\\[0ex]4. $g$ : $A$$\rightarrow$$B$
\\[0ex]5. $\forall$$x$:$A$. ($\neg\neg$($f$($x$) = $g$($x$))) $\Rightarrow$ ($f$($x$) = $g$($x$))
\\[0ex]6. $\neg\neg$($f$ = $g$)
\\[0ex]7. $x$ : $A$
\\[0ex]$\vdash$  $\neg\neg$($f$($x$) = $g$($x$))